$\forall$$T$:Type. $T$ $\subseteq\rho$ $\mathbb{Z}$ $\Rightarrow$ ($\forall$$x$:$T$, $L$:$T$ List. s{-}insert($x$;$L$) $\in$ $T$ List)